package stackSample;

import gov.nasa.jpf.jvm.Verify;

import java.util.ArrayList;
import java.util.List;

public class StackDriver {

	public static void main(String[] args) {
		Stack state = new Stack();
		/*
		 * i denotes the i_th method call
		 * against one stack object
		 */
		for (int i = 1; i <= 3; i++) {

			/**
			 * pre-condition
			 */
			List<Integer> opts = new ArrayList<Integer>();
			if (!state.popPre()) {
				opts.add(new Integer(1));
			}
			if (!state.pushPre()) {
				opts.add(new Integer(2));
			}

			int[] optsPre = new int[opts.size()];
			for (int k = 0; k < optsPre.length; k++) {
				optsPre[k] = opts.get(k).intValue();
			}
			
			int index = Verify.getInt(0, opts.size() - 1);
			int method = opts.get(index);
			
			try {
				switch (method) {
				case 1:
					state.pop();
					break;
				case 2:
					state.push(1);
					break;
				default:
					break;
				}
			} catch (RuntimeException _) {
				//TODO handle exception
			}

			/**
			 * post-condition
			 */
			opts = new ArrayList<Integer>();
			if (!state.pushPre()) {
				opts.add(new Integer(2));
			}
			if (!state.popPre()) {
				opts.add(new Integer(1));
			}

			int[] optsPost = new int[opts.size()];
			for (int k = 0; k < optsPost.length; k++) {
				optsPost[k] = opts.get(k).intValue();
			}

			boolean postIsNew = InterfaceGenerator.updateFSM(optsPre, optsPost);
			Verify.ignoreIf(!postIsNew);
		}
		
	}

}
